f1(X) -> cons2(X, n__f1(g1(X)))
g1(0) -> s1(0)
g1(s1(X)) -> s1(s1(g1(X)))
sel2(0, cons2(X, Y)) -> X
sel2(s1(X), cons2(Y, Z)) -> sel2(X, activate1(Z))
f1(X) -> n__f1(X)
activate1(n__f1(X)) -> f1(X)
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
f1(X) -> cons2(X, n__f1(g1(X)))
g1(0) -> s1(0)
g1(s1(X)) -> s1(s1(g1(X)))
sel2(0, cons2(X, Y)) -> X
sel2(s1(X), cons2(Y, Z)) -> sel2(X, activate1(Z))
f1(X) -> n__f1(X)
activate1(n__f1(X)) -> f1(X)
activate1(X) -> X
SEL2(s1(X), cons2(Y, Z)) -> ACTIVATE1(Z)
SEL2(s1(X), cons2(Y, Z)) -> SEL2(X, activate1(Z))
F1(X) -> G1(X)
ACTIVATE1(n__f1(X)) -> F1(X)
G1(s1(X)) -> G1(X)
f1(X) -> cons2(X, n__f1(g1(X)))
g1(0) -> s1(0)
g1(s1(X)) -> s1(s1(g1(X)))
sel2(0, cons2(X, Y)) -> X
sel2(s1(X), cons2(Y, Z)) -> sel2(X, activate1(Z))
f1(X) -> n__f1(X)
activate1(n__f1(X)) -> f1(X)
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
SEL2(s1(X), cons2(Y, Z)) -> ACTIVATE1(Z)
SEL2(s1(X), cons2(Y, Z)) -> SEL2(X, activate1(Z))
F1(X) -> G1(X)
ACTIVATE1(n__f1(X)) -> F1(X)
G1(s1(X)) -> G1(X)
f1(X) -> cons2(X, n__f1(g1(X)))
g1(0) -> s1(0)
g1(s1(X)) -> s1(s1(g1(X)))
sel2(0, cons2(X, Y)) -> X
sel2(s1(X), cons2(Y, Z)) -> sel2(X, activate1(Z))
f1(X) -> n__f1(X)
activate1(n__f1(X)) -> f1(X)
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
G1(s1(X)) -> G1(X)
f1(X) -> cons2(X, n__f1(g1(X)))
g1(0) -> s1(0)
g1(s1(X)) -> s1(s1(g1(X)))
sel2(0, cons2(X, Y)) -> X
sel2(s1(X), cons2(Y, Z)) -> sel2(X, activate1(Z))
f1(X) -> n__f1(X)
activate1(n__f1(X)) -> f1(X)
activate1(X) -> X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G1(s1(X)) -> G1(X)
POL(G1(x1)) = 2·x1
POL(s1(x1)) = 1 + 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
f1(X) -> cons2(X, n__f1(g1(X)))
g1(0) -> s1(0)
g1(s1(X)) -> s1(s1(g1(X)))
sel2(0, cons2(X, Y)) -> X
sel2(s1(X), cons2(Y, Z)) -> sel2(X, activate1(Z))
f1(X) -> n__f1(X)
activate1(n__f1(X)) -> f1(X)
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
SEL2(s1(X), cons2(Y, Z)) -> SEL2(X, activate1(Z))
f1(X) -> cons2(X, n__f1(g1(X)))
g1(0) -> s1(0)
g1(s1(X)) -> s1(s1(g1(X)))
sel2(0, cons2(X, Y)) -> X
sel2(s1(X), cons2(Y, Z)) -> sel2(X, activate1(Z))
f1(X) -> n__f1(X)
activate1(n__f1(X)) -> f1(X)
activate1(X) -> X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SEL2(s1(X), cons2(Y, Z)) -> SEL2(X, activate1(Z))
POL(0) = 2
POL(SEL2(x1, x2)) = x1 + x2
POL(activate1(x1)) = 1 + x1
POL(cons2(x1, x2)) = 1 + 2·x2
POL(f1(x1)) = 1
POL(g1(x1)) = 1 + x1
POL(n__f1(x1)) = 0
POL(s1(x1)) = 1 + 2·x1
f1(X) -> cons2(X, n__f1(g1(X)))
activate1(n__f1(X)) -> f1(X)
activate1(X) -> X
f1(X) -> n__f1(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f1(X) -> cons2(X, n__f1(g1(X)))
g1(0) -> s1(0)
g1(s1(X)) -> s1(s1(g1(X)))
sel2(0, cons2(X, Y)) -> X
sel2(s1(X), cons2(Y, Z)) -> sel2(X, activate1(Z))
f1(X) -> n__f1(X)
activate1(n__f1(X)) -> f1(X)
activate1(X) -> X